package list3;

public class List {
	/*@ rep  @*/ Entry first;
	
	public void add(/*@ readonly @*/ Object o) {
		first = new /*@ rep @*/ Entry(o, null, first);
		System.out.println("Added: " + o);
	}
	
	// Universe Types with Transfer
	/*@ pure @*/
	public /*@ free @*/ ListIter iterator() {
		return new /*@ free @*/ ListIterImpl(this);
	}
	
	//@ requires cur.owner == this;
	public void remove(/*@ readonly @*/ Entry cur) {
		// If the precondition holds, then this cast is successful
		/*@ rep @*/ Entry re = (/*@ rep @*/ Entry) cur;
		
		// Actually remove the entry...
		System.out.println("Entry not really removed...");
	}
}

class Entry {
	/*@ peer @*/ Entry prev, next;
	/*@ readonly @*/ Object data;
	
	public Entry(/*@ readonly @*/ Object o, /*@ peer @*/ Entry p, /*@ peer @*/ Entry n) {
		data = o;
		prev = p;
		next = n;
	}
}